The notion of strong dinatural transformation is a notion of natural transformation between pairs of functors that is stronger than that of dinatural transformations.
Unlike dinatural transformations, strong dinatural transformations can always be composed. They have close connections to parametricity in computer science.
Let be functors. A strong dinatural transformation consists of, for each , a component , such that for any morphism in and any span in , if the square on the left commutes, then the outer hexagon also commutes:
If the pullback exists in , it suffices to assert this when the square on the left is the defining one of that pullback. On the other hand, if has a separator (such as ), it suffices to assert this when is the separator.
By comparison, a dinatural transformation asserts this condition only when with the span consisting of and .
We can regard strong dinatural transformations as a variation on the relational approach to parametric polymorphism, as follows.
If and has finite limits then for every in we can regard the pullback as a relation
From this point of view, the family is strong dinatural if and only if it preserves these relations, i.e.
As shown by Vene (2006), for a class of types, the usual relational interpretation corresponds to a strong dinaturality interpretation.
However, the strong dinatural transformations don’t form a Cartesian closed category in general (e.g. Uustalu 2010) so might not serve to interpret all types, including function types.
Originally introduced (as “strong dinatural transformations”) in Definition 2.7 of:
Further developments:
Philip S. Mulry: Strong monads, algebras and fixed points, Applications of Categories in Computer Science 177 (1992) 202–216 [doi:10.1017/CBO9780511525902.012]
Robert Paré, Leopoldo Román: Dinatural numbers. Journal of Pure and Applied Algebra 128 1 (1998) 33–92 [doi:10.1016/S0022-4049(97)00036-4]
A. Eppendahl, Parametricity and Mulry’s Strong Dinaturality, Department of Computer Science Technical Report No 768, Queen Mary (1999) [pdf, ISSN:1369-1961]
Varmo Vene: Parametricity and Strong Dinaturality, talk notes (2006) [pdf, archive:pdf]
Jennifer Hackett, Graham Hutton: Programs for cheap!, In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 115–126 [doi:10.1109/LICS.2015.21]
Tarmo Uustalu: Strong dinaturality and initial algebras 12th Nordic Wksh. on Programming Theory, NWPT 2 (2000).
Tarmo Uustalu: A Note on Strong Dinaturality, Initial Algebras and Uniform Parameterized Fixpoint Operators, In: FICS 2010. 77–82 [pdf, pdf]
Strong dinatural transformations are called paranatural transformations in:
Last revised on July 25, 2024 at 16:58:39. See the history of this page for a list of all contributions to it.